EasyCrypt Circuit Based Reasoning Extension by Gustavo2622 · Pull Request #752 · EasyCrypt/easycrypt

Gustavo2622 · 2025-03-18T14:27:19Z

Adds circuit based reasoning to EasyCrypt in the form of a module for converting EC constructs into circuits and reasoning over said circuits.
Adds various tactics to use the added functionality in proofs.
Depends on external SMT solver BitWutzla and on external circuit library Lospecs.

strub · 2026-01-20T12:56:51Z

easycrypt.opam

  "why3" {>= "1.8.0" & < "1.9"}
+  "ppx_deriving"
+  "ppx_deriving_yojson"
+  "hex"


Do we really need these 4 last dependencies?

Both ppx_derivings were for the printing of spec language ASTs, we can add a custom printing method to replace it. Hex was for the parsing of hexadecimal integers in the spec language, so that one seems wise to keep instead of rolling our own

strub · 2026-01-20T12:57:51Z

dune

@@ -1,4 +1,9 @@
-(dirs 3rdparty src etc theories examples assets scripts)
+(env


Move the OCaml flags from src so that we use the same flags everywhere.

strub · 2026-01-20T12:58:05Z

config/tests.config

 [test-examples]
 okdirs  = !examples
-exclude = examples/MEE-CBC examples/old examples/old/list-ddh !examples/incomplete examples/to-port
+exclude = examples/MEE-CBC examples/exclude examples/old examples/old/list-ddh !examples/incomplete examples/to-port


What the point of adding examples that are directly excluded?

No point, that line was changed in a commit that was removing examples dependent on JWord, so ideally we remove both

strub · 2026-01-20T12:59:10Z

flake.nix

@@ -4,22 +4,23 @@



Why this file is modified at all?

These are change I made locally to make it actually work, it should not be part of this PR (but it is rather useful, so we can think about if we want to propagate some version of them)

strub · 2026-01-20T13:04:32Z

src/ecCircuits.ml

+    in
+    doit {level = 0; subst = EcSubst.empty} f
+
+  (* FIXME: Check that this does not incur false positives *)


Solve FIXME

strub · 2026-01-20T13:14:58Z

src/ecCoreFol.mli

 val f_pr   : memory -> xpath -> form -> ss_inv -> form

+(* FIXME: Check this V *)
+(* FIXME CIRCUIT PR: do we want to keep this? *)


strub · 2026-01-20T13:15:03Z

src/ecCoreFol.mli

+val ty_chunk   : ty -> ty
+val ty_all     : ty -> ty
+
+(* FIXME CIRCUIT PR: if keeping, maybe change names *)


strub · 2026-01-20T13:15:29Z

src/ecDecl.ml

+  ; size   : binding_size
+  ; theory : EcPath.path }
+
+type bv_opkind = [


Should we use a non-variant-polymorphic datatype?

Non-polymorphic variant?

strub · 2026-01-20T13:16:22Z

src/ecEnv.ml

  sp_params : int * (EcIdent.t * module_type) list;
 }

-


This file as a lot of modifications that are not related to bdep. Problem with merge?

Might be, but there was a reordering of the file contents needed by bdep, so that might be confusing the diff (or might have confused the merge algo)

strub · 2026-01-20T13:16:45Z

src/ecHiTacticals.ml

  FApi.t_try (process1_core ttenv t) tc

+(* -------------------------------------------------------------------- *)
+(* FIXME: Maybe move the extens tactic to this file as well? *)


Was creating a dependency loop when I first tried to put it there, but might have been because of some debugging instructions, we can move before the merge

Gustavo2622 added enhancement library tactics labels Mar 18, 2025

Gustavo2622 requested a review from strub March 18, 2025 14:27

Gustavo2622 self-assigned this Mar 18, 2025

Gustavo2622 force-pushed the bdep_ecCircuitsRefactor branch 3 times, most recently from 1b12249 to 66efdd7 Compare March 24, 2025 16:44

Gustavo2622 force-pushed the bdep_ecCircuitsRefactor branch from fdefb72 to 7ec289f Compare March 31, 2025 20:40

Gustavo2622 force-pushed the bdep_ecCircuitsRefactor branch 2 times, most recently from aef3a2b to 01f21ac Compare August 8, 2025 11:15

Gustavo2622 force-pushed the bdep_ecCircuitsRefactor branch from 58c193f to 433cbb4 Compare August 19, 2025 08:24

Gustavo2622 force-pushed the bdep_ecCircuitsRefactor branch 3 times, most recently from d7c187a to f433cb0 Compare September 8, 2025 14:24

Gustavo2622 changed the title ~~EasyCrypt Circuit Based Reasoning Extension~~ EasyCrypt Circuit Based Reasoning Extension (NOT UP TO DATE) Sep 14, 2025

Gustavo2622 changed the title ~~EasyCrypt Circuit Based Reasoning Extension (NOT UP TO DATE)~~ EasyCrypt Circuit Based Reasoning Extension Sep 14, 2025

Gustavo2622 force-pushed the bdep_ecCircuitsRefactor branch from 8288caf to 57a2e2b Compare September 17, 2025 15:19

Gustavo2622 force-pushed the bdep_ecCircuitsRefactor branch from 5b0ce21 to d299f15 Compare December 4, 2025 00:13

Circuit reasoning functionality

bada5a0

Gustavo2622 force-pushed the bdep_ecCircuitsRefactor branch from a828b25 to bada5a0 Compare January 20, 2026 12:47

strub requested changes Jan 20, 2026

View reviewed changes

Gustavo2622 added 4 commits January 22, 2026 20:34

First pass on new error reporting

1cbd638

Added implicit type translation

60eb802

Added duplicate checking for spec files and general cleanup

267854c

Merge remote-tracking branch 'origin/main' into bdep_ecCircuitsRefactor

60577ad

		@@ -1,4 +1,9 @@
		(dirs 3rdparty src etc theories examples assets scripts)
		(env

Conversation

Gustavo2622 commented Mar 18, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants